\begin{tabbing}
$\forall$${\it es}$, $C$, $T$, $S$, $R$, ${\it codes}$, ${\it decodes}$, ${\it Req}$, ${\it Ack}$:Top.
\\[0ex]for\= clients $C$ sends FIFO\+
\\[0ex]from j to i via ($S$[j,i],${\it codes}$)
\\[0ex]receives at i via ($R$[i],${\it decodes}$)  requests ${\it Req}$[j] are acknowledged by ${\it Ack}$[j,i]
\-\\[0ex]$\sim$
\\[0ex]($\forall$$i$:$C$.
\\[0ex]$\exists$\=$f$:\{$e$:E$\mid$ $R$($i$,$e$)\} $\rightarrow$\{$e$:E$\mid$ $\exists$$j$:$C$. ($S$($j$,$i$,$e$))\} \+
\\[0ex]fifo+property(${\it es}$;${\it codes}$;${\it decodes}$;$C$;$S$;$R$;$T$;${\it Req}$;${\it Ack}$;$i$;$f$))
\-
\end{tabbing}